es:ES, ff:FIFO, p:(E), e:E, sndr, rcvr:ff.C. [e: sndr p rcvr]   

latex

Definitions	x:A. B(x), FIFO, , t  T, [e: i p j], P & Q, A c B
Lemmas	fifoC wf, es-E wf, es-state wf, es-loc wf, fifo wf, event system wf